Note: The numbers attached to each option represents the corresponding options under batch mode verification and command line console.

Deadlock-Freeness, Deterministic, Divergence-Freeness, Nonterminating, Reachability and Safety-LTL Properties:

• Admissible behaviors: All (0)
• Verification engines:
  • First witness trace using Depth First Search (0)
  • Shortest witness trace using Breadth First Search (1)

Properties with probability calculation:

• Admissible behaviors: All (0)
• Verification engines:
  • Graph-based probability computation based on value iteration (0)

Refinement:

• Adimissible behaviors: All (0)
• Verificaition engines:
  • On-the-fly trace refinement checking using Depth First Search (0)
  • On-the-fly trace refinement checking using Breadth First Search (1)

Failure-Refinement:

• Adimissible behaviors: All (0)
• Verificaition engines:
  • On-the-fly failure refinement checking using Depth First Search (0)
  • On-the-fly failure refinement checking using Breadth First Search (1)

Failure/Divergence Refinement:

• Adimissible behaviors: All (0)
• Verificaition engines:
  • On-the-fly failures/divergence refinement checking using Depth First Search (0)
  • On-the-fly failures/divergence refinement checking using Breadth First Search (1)

Liveness Properties without probability calculation:

• Adimissible behaviors:
  • All (0)
  • Event-level weak fair only (1)
  • Event-level strong fair only (2)
  • Process-level weak fair only (3)
  • Process-level strong fair only (4)
  • Global fair only (5)
• Verificaition engines (same for each adimissible behaviors above):
  • Strongly connected components based search (0)